\begin{tabbing}
${\it es}$ $\equiv$ ${\it es'}$ mod ${\it es}$,$e$.$P$(${\it es}$;$e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=\{$e$:es{-}E(${\it es}$)$\mid$ $P$(${\it es}$;$e$)\}  $\equiv$ \{$e$:es{-}E(${\it es'}$)$\mid$ $P$(${\it es'}$;$e$)\} \+
\\[0ex]\& (\=$\forall$$e$:\{$e$:es{-}E(${\it es}$)$\mid$ $P$(${\it es}$;$e$)\} .\+
\\[0ex]es{-}kind(${\it es}$; $e$) = es{-}kind(${\it es'}$; $e$) $\in$ Knd \& es{-}loc(${\it es}$; $e$) = es{-}loc(${\it es'}$; $e$) $\in$ Id)
\-\\[0ex]\& (\=$\forall$$e_{1}$:\{$e$:es{-}E(${\it es}$)$\mid$ $P$(${\it es}$;$e$)\} , $e_{2}$:\{$e$:es{-}E(${\it es}$)$\mid$ $P$(${\it es}$;$e$)\} .\+
\\[0ex](es{-}causl(${\it es}$; $e_{1}$; $e_{2}$) $\Leftarrow\!\Rightarrow$ es{-}causl(${\it es'}$; $e_{1}$; $e_{2}$))
\\[0ex]\& (es{-}same{-}val(${\it es}$;$e_{1}$;$e_{2}$) $\Leftarrow\!\Rightarrow$ es{-}same{-}val(${\it es'}$;$e_{1}$;$e_{2}$)))
\-\-
\end{tabbing}